Typically, software analysts have some security objectives in mind and want to verify that the software meets these objectives. In order to do this, a security analyst would typically analyze the source code or the binary code using some tools, such as static analysis or formal verification. It is well-known that there is a gap between these informal security objectives and the formal properties that can be verified using these tools. In other words, the property that the analyst actually checks using these tools could differ from the security objectives that she intended to verify. In order to be confident in her results, the analyst needs to ensure that the verified formal properties imply the intended security objectives. Often, the reasoning behind this step would exist only in the analyst's head and is lost after the verification. Similarly, the security objective itself is often lost. Only formal properties are left. Unfortunately, it is difficult to read the formal properties and to understand the connection between desired informal properties and verifiable formal ones. Therefore, it is hard to recheck the software and there is no way to confirm that the low-level properties actually match the high-level objective.
Thus, a continuing need exists for a system that fills the gap between high-level informal desired security properties and low-level formal verifiable properties, thereby enabling an analyst to verify that a particular software application meets desired security objectives.